1. Technical Field
This disclosure generally relates to constraint solvers. More specifically, this disclosure relates to methods and apparatuses for rewriting constraints.
2. Related Art
The importance of circuit verification cannot be over-emphasized. Indeed, without circuit verification it would have been impossible to design complicated integrated circuits which are commonly found in today's computing devices.
Constrained random simulation methodologies have become increasingly popular for functional verification of complex designs, as an alternative to directed-test based simulation. In a constrained random simulation methodology, random vectors are generated to satisfy certain operating constraints of the design. These constraints are usually specified as part of a test-bench program. A test-bench automation tool (TBA) uses the test-bench program to generate random solutions for a set of random variables, such that a set of constraints over the set of random variables is satisfied. These random solutions can then be used to generate valid random stimulus for the Design Under Verification (DUV). This stimulus is simulated using simulation tools, and the results of the simulation are typically examined within the test-bench program to monitor functional coverage, thereby providing a measure of confidence on the verification quality and completeness.
Constraint solvers are typically used to generate random vectors that satisfy the set of constraints. The basic functionality of a constraint solver is to solve the following constraint satisfaction problem: given a set of random variables and a set of constraints, assign a set of random values to the set of random variables that satisfy the set of constraints. For better software maintenance and quality, the solutions generated by the constraint solver need to be reproducible and deterministic. Further, since users typically require good coverage for the random simulation, the constraint solutions also need to satisfy a user provided distribution.
Unfortunately, the constraint satisfaction with desired solution distribution problem is NP-hard. Logic simulation, on the other hand, usually scales linearly with the size of the design. As a result, the speed of stimulus generation usually lags far behind the speed at which the stimulus is used in the simulation. Hence, it is desirable to improve performance of a constraint solver because it can significantly improve the overall performance of constrained random simulation tools.